FDL - Nuprl Lemma : last-state-change3

Nuprl Lemma : last-state-change3

es:ES, ds:x:Id fp

Type, T:Type, i:Id, f:(State(ds)

T).
(

x, y:T. Dec(x = y))

@i discrete ds

e'@i.

(

e:E. e

loc e'

(f((discrete state when e)) = f((discrete state after e'))

T))

(

e:E

(

(e

loc e'

(

c

((

(f((discrete state when e)) = f((discrete state after e'))))

(

c

& (

e'':E.

(

c

& ((e <loc e'')

(

c

& (

e''

loc e'

(

c

& (

(f((discrete state when e'')) = f((discrete state after e'))

T)))))

Definitions x:A. B(x), P Q, e@i. P(e), P Q, e loc e' , x:A. B(x), A c B, P & Q, (e <loc e'), , t T, x. t(x), {T}, T, True, State(ds), discrete state@i, A, P Q, x(s), SQType(T), P Q, Dec(P), False

Lemmas alle-at-iff, es-locl wf, es-dstate-when wf, es-dstate-subtype, es-loc wf, es-le-loc, Id sq, es-dstate-after wf, not wf, es-causl wf, es-loc-pred, es-locl-iff, assert wf, es-first wf, es-dds wf, decidable wf, decl-state wf, Id wf, fpf wf, event system wf, es-le wf, es-le-iff, squash wf, true wf, es-E wf, es-le weakening eq, es-locl transitivity2, es-locl irreflexivity, es-le-pred, dstate-after-pred, ifthenelse wf, es-isconst wf, es-vartype wf, top wf, fpf-cap wf, id-deq wf, equal functionality wrt subtype rel, es-pred-locl, es-locl transitivity1, es-le weakening